STM: updates of wf

STM: updates of append

ABS: consistent-updates(es;In;Out;Cmd;isupdate;expl)

STM: consistent-updates wf

ABS: is-query(In;isupdate;e)

STM: is-query wf

ABS: approx_sm(es; In; Out; Cmd; isupdate; Rsp; Delta; Q)

STM: approx sm wf

ABS: sys-antecedent(es;Sys)

STM: sys-antecedent wf

STM: sys-antecedent-retraction

ABS: fifo-antecedent(es;Sys;f)

STM: fifo-antecedent wf

STM: fifo-antecedent-order-preserving

ABS: effective(e)

STM: cr-effective wf

ABS: chain-config(es;Sys;chain)

STM: chain-config wf

STM: chain-config-reverse

ABS: chain-consistent(f;chain)

STM: chain-consistent wf

STM: chain-consistent-member

STM: chain-consistent-after-input

STM: chain-consistent-prior-to-input

ABS: x << y

STM: chain-order wf

STM: chain-order-antisymmetric-config

STM: chain-order-antisymmetric

STM: chain-order-antireflexive

STM: chain-order-implies-before

STM: chain-order transitivity

STM: chain-order-total-config

STM: chain-order-total

STM: chain-order-total2

ABS: x <<= y

STM: chain-order-le wf

STM: chain-order-le transitivity

STM: chain-order transitivity2

STM: chain-order transitivity3

STM: chain-order-le antisymmetry

STM: chain-order-in-out

STM: chain-path-ordered

STM: chain-path-ordered-same-loc

STM: chain-path-ordered-same-loc2

STM: chain-path-ordered-same-loc3

STM: chain-path-member-not-input

STM: chain-path-query

STM: chain-pullback

STM: chain-consistent-continuity

STM: chain-consistent-out-continuity

STM: chain-consistent-effective-continuity

ABS: x fails-before y

STM: cr-fails-before wf

STM: chain-consistent-fails-before

STM: chain-consistent-fails-before2

STM: chain-consistent-fails-before3

STM: chain-consistent-monotone-lemma0

STM: chain-consistent-continuity2

ABS: sys-order(es;Sys;f)

STM: sys-order wf

STM: chain-consistent-order

ABS: explanation(e)

STM: cr-explanation wf

STM: cr-explanation-step

STM: cr-explanation-connected

STM: chain-consistent-updates1

STM: cr-explanation-es-le

STM: chain-consistent-updates

ABS: e did forward 

STM: did-forward wf

ABS: a should forward 

STM: should-forward wf

ABS: input-forwarding(es;Cmd;Sys;isupdate;In;f)

STM: input-forwarding wf

STM: filter-updates-lemma

STM: chain-consistent-same-sender

STM: chain-consistent-same-receiver

STM: input-forwarding-invariant

ABS: abstract-chain-replication{i:l}(es;Cmd;Rsp;isupdate;In;Out;Sys;f;Delta;Q)

STM: abstract-chain-replication wf

STM: abstract-chain-replication-property

ABS: chain-replication-acks{i:l}(es;Cmd;Rsp;isupdate;In;Out;Sys;Ack;f;g;Delta;Q)

STM: chain-replication-acks wf

STM: chain-replication-acks-refines

STM: acks-chain-consistent

STM: chain-consistent-input-continuity

STM: chain-consistent-dual-continuity